COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		PROPOSAL
C00012 00003	
C00022 ENDMK
C⊗;
	PROPOSAL
           in
VERIFICATION ORIENTED PROGRAMMING


1.  INTRODUCTION

This is a  proposal to undertake  research into both  theoretical and
practical   problems   associated   with   programming  methods   and
techniques.  The main  emphasis is to  be the development of  on-line
systems  providing  assistance  in the  specification,  construction,
documentation, and maintenance of programs. 


Our proposal is based on two sources of recent technical advancement. 
(The outline given here will  be explained in detail in  Section 2). 
First,there  are  a  number  of  significant  contributions  directed
towards giving precise axiomatic definitions of the semantics of  actual
(implemented) programming  languages,  and related  studies aimed  at
making  a  science  of programming  methodology.    In particular  we
mention the  work of  Hoare, Wirth,  Brinch-Hansen, Clint,  Dijkstra,
Dahl,  [see references...].    Secondly,  there is  the  work at  the
Stanford  A.I.   Lab  carried  out over  the  past two  years  in the
development of the Stanford PASCAL Verification System.   This system
has already  been applied successfully to  debugging, documenting and
verifying programs in  several different application  areas. It   has
yielded very promising  lines of attack on the problem of developing 
 new accurate techniques  for   dealing  with  the verification and 
documentation of programs. [see
references....].   It  has  been  clearly shown  in  this  work  that
theoretical advances in  the design of programming  languages and the
specification   of  their  semantics  can  be  directly  utilized  in
developing  systems for  automating  the  verification  of  programs.
Further such verification systems  can be used to provide on-line aid
to programmers in debugging and documenting programs. 

These developments  are  the  point  of  departure  for  the  present
proposal.   In  brief outline,  we are  proposing  research into  the
following areas. 

I.  THEORY OF PROGRAMMING:

(a) Axiomatic semantics of programming languages. 

(b) Verification  techniques and  methods (program documentation  and
    program proving).  

(c) Design of verification-oriented programming languages. 


II.  DEVELOPMENT OF ON-LINE PROGRAMMING AIDS.

(a) PASCAL documentation and verification system. 

(b) Extended specification compiler. 

(c) Program manipulation command languages. 

We explain exactly what  is covered by  these headings in Section  3.
The points to be emphasized here are:

(i)  Recent theorectical  work  provides a  framework for  developing
precise  program verification aids, thus  providing a new programming
technique  to augment  (  not  replace) the  existing  repertoire  of
techniques; Part II  of the proposal is to push  the development of a
verification system  (together  with applications  to  debugging  and
documentation) for a  widely used multipurpose  programming language,
and to research  the problem of integrating it with other programming
aids. 

(ii) Much  theoretical  research  remains  to be  done  in  designing
programming languages oriented towards the construction of verifiable
and  robust  programs,  especially  in  complex  task  areas such  as
operating systems programming.  At the present time, such theoretical
research   is  probably   best  undertaken   hand-in-hand   with  the
development of practical verification  systems so that the  practical
advantages of design decisions can be tested,  and conversely so that
design  decisions arising  from practical  problems  can be  based on
sound general principles.   Part  I of the  proposal involves  theory
associated  with extensions  of  the verification  system  (e.g.   to
parallel  processes), with elucidating the relative merits of various
methods of program specification, documentation and verification, and
with  the incorporation of  verification information  explicitly into
the programming language. 


(iii) The  need  in all  sectors  of computer  utilization  for  more
accurate programming methodology  in all four  phases (specification,
construction,  documentation, maintenance) has  been widely discussed
(often in terms of reducing the high cost of software).  The proposal
is ultimately directed toward satisfying this need. 




2. PERSPECTIVE

***recent history and progress



**programming languages and methods.**
This survey is to include early work:Floyd→Hoare→wirth leading to 
  axiomatic pascal, and verification systems.
Dahl(simula classes) a scheme concept leading to monitors.
Dijkstra,Hoare,dahl→ leading to structuring principles in programming 
Dijkstra(semaphores)→Brinch-Hansen&Hoare(monitors)→ leading to
concurrent pascal.
Habermann monitor invariants, and path expressions → leading to 
definition of proof techniques for parallel processes.
Wulf (alphard)forms → scheme concept similar to Dahl used to provide 
explicit abstraction for  use in defining data structures, processes
with rights& restrictions.

**verification systems**
First system King,Floyd & King→ possibility of automating proving properties
of interesting programs(sorting etc.)
Further work by Deutsch, and Elspas, Levitt,&Waldinger, and Igarashi,London
Luckham carries the approach of King-Floyd
→ leading to automation of parts of the verification problem.
In particular, the Igarashi,london,Luckham VCG for pascal is 
based specifically on the axiomatic semantics of the language
and is easily extended to include modifications of the language
or to deal with other languages which possess similar kinds of semantics
(e.g. Algol).
As a result, we now underatand how to design verification  systems for 
specific languages.
Further work Suzuki shows the possibility of standardizing the proofs of
hard sorting programs.
v. Henke&Luckham develops the debugging and documentation applications
of verifiers.

** description of the current STANFORD PASCAL VERIFIER**  

3. PROPOSED RESEARCH


***MOTIVATIONAL CONNECTIONS:
(a). semantics and proof theory of concurrent PAscal
←VCG use of such axiomatic defs.
(B). extension of PAscal to include more user Abstraction constructs
←use by fast prover, methodology of structured programming.
(C). Analysis of programs: on-line analysis of VC's, proof tracing
etc...←methodology
(D) applications
(E) program manipulation language


*** expansion of  headings above into subheadings
*** explanation ofpossibilities   under  each  subheading
***  practical  development commitments



(a) Axiomatic Semantics of Programming Languages. 

Axiomatic semantics, such as the PASCAL definition  [Hoare and Wirth]
need to be found for  many concepts and constructors not contained in
current versions  of programming  languages.   Such  extensions  must
preceed  developing  a rigorous  programming  methodology  (including
structuring, verification, documentation, and  automated programming)
and the  extension  of languages  such  as  PASCAL into  high  level
languages for  implementing various kinds  of systems programs.   We
mention the  following topics as being among those for which we shall
study the axiomatic semantics. 

	  (i) important  commonly  implemented  data  structures  for
example,  POINTERS, RECORDS..... (This  affects the  verification and
documentation of many existing programs). 

	 (ii) User-defined abstract data structures (directed towards
precise structuring techniques in programming). 
	 
	(iii)   New  programming   language   constructs,   including
COROUTINES,    MONITORS,   GUARDED   STATEMENTS,    ON   and   ENABLE
CONDITIONS....  Axiomatic  semantics for  some of these  constructors
have already been given; these studies are far from adequate, and the
inter-relations  between the  various constructors still  needs to be
investigated (Directed in particular at the verification of operating
systems and the design of high-level systems programming languages.)

	(b) Verification Techniques and Methods

This heading  covers two distinct  areas, the theory  of constructing
the tools (i.e.   various parts of  systems) for on-line  programming
aids,  aad  the  theory  of  how  to  use  the  tools.    Significant
contributions have already been made in the first area, which we now
regard as a  "developing field", but  the second  area appears to  be
totally open. 

Below,  topics (i)  aad (ii)  are relevant  to the  second area  (and
progress  in (ii)  will be  very much  a function of  decisions taken
under (i)); topics (iii) fall in the first area. 

	  (i)  Design of  Assertion  Langauges  -  Current  assertion
languages  used for specifying  and documenting programs  are derived
from languages for formal logic.   Many programming concepts have  no
natural easy representation in these  languages.  Assertion languages
must be developed so that programmers can state concisely information
they possess about their programs, e.g.  statements  about underlying
data structures  (c.f.(a(iii)) such as  "array A is a  permutation of
array  B", properties  of history  sequences of values  of variables,
bounds on computation times, and relationships between  programs.  In
particular,  the ability to  document a  program by means  of another
program needs to be developed and understood (see [Clint], [Henke and
Luckham]). 

	 (ii) Structuring  of Proofs and Documentation of  Programs -
Here  we wish to  develop general standards  for documenting programs
and proving properties of them.  There are two parts to  the problem:
setting up the  standards and giving methods for attaining  them.  We
shall  try  to approach  this by  building  on already  defined basic
concepts: the  BASIS  of  a Verification,  ADEQUACY  of a  BASIS  and
ACCEPTABILITY of  a BASIS [see Henke  and Luckham].   Our approach to
the  methodology  is   that  the   construction,  documentation   and
verification   of  programs   are   complementary  and   simultaneous
processes,  that  the top-down  structure  of the  program  imposes a
similar structure on  the correctness proof,  and that an  acceptable
basis for the proof of one  level provides the documentation for that
level  and the specifications for the next  lower level.  The methods
for  expanding (or  "filling  in")  documentation depend  on  on-line
analysis of  what is  required to complete  a correctness proof  of a
level in a program.   The analysis depends  on what on-line aids  are
available (see  (iii)).   This is  a topic  of research  where it  is
absolutely  essential that the  theory be  developed in the  light of
experimental testing.    Ultimately we  hope  to provide  an  on-line
system  which  permits  the  programmer to  carry  out  construction,
verification and documentation as a unified activity. 


	  (iii) Techniques  of  Program Proving  - This  involves the
theory of  proving  properties of  programs  the objective  being  to
automate as much of this  as possible.  Results in this area are very
much dependant on  the representation  of the problem  to be  proved,
namely the programming language and the  assertion language (i.e. (a)
and  (b,i)).  Among  the relevant  topics that require  further study
are: 1.   The proof theory of  the logic of  programs implied by  the
axiomatic semantics, especially the  semantics of new constructs (see
[Igarashi, London,  Luckham] for a study which provided the basis for
Verification Condition  Generation);  2.   The  use of  documentation
statements  to   construct  special  purpose   proof  procedures;  3.
Application  of  general  theorem-proving  programs  to   verification
problems. 
	







4.  LABORATORY FACILITIES AND BUDGET